(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 16))
(declare-fun a1 () (Array  (_ BitVec 13)  (_ BitVec 16)))
(declare-fun a2 () (Array  (_ BitVec 10)  (_ BitVec 13)))
(assert (let ((e3(_ bv1 1)))
(let ((e4(_ bv849 10)))
(let ((e5 (bvnot e3)))
(let ((e6 ((_ rotate_left 3) e4)))
(let ((e7 (ite (bvsle e6 e4) (_ bv1 1) (_ bv0 1))))
(let ((e8 (ite (bvult ((_ sign_extend 6) e6) v0) (_ bv1 1) (_ bv0 1))))
(let ((e9 (store a2 ((_ extract 13 4) v0) ((_ zero_extend 12) e7))))
(let ((e10 (store e9 ((_ sign_extend 9) e5) ((_ sign_extend 12) e7))))
(let ((e11 (store a1 ((_ zero_extend 12) e3) ((_ zero_extend 15) e5))))
(let ((e12 (select e9 ((_ sign_extend 9) e5))))
(let ((e13 (select e10 ((_ extract 13 4) v0))))
(let ((e14 (store a2 ((_ zero_extend 9) e7) ((_ sign_extend 12) e3))))
(let ((e15 (select a2 ((_ extract 12 3) e13))))
(let ((e16 (store a2 ((_ sign_extend 9) e8) ((_ sign_extend 12) e7))))
(let ((e17 (ite (bvsge e13 e15) (_ bv1 1) (_ bv0 1))))
(let ((e18 (bvsrem v0 v0)))
(let ((e19 (ite (= e12 ((_ zero_extend 3) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e20 (bvlshr ((_ sign_extend 12) e5) e15)))
(let ((e21 (bvxor ((_ sign_extend 12) e7) e12)))
(let ((e22 (ite (= (_ bv1 1) ((_ extract 0 0) e8)) e5 e5)))
(let ((e23 (bvand e15 ((_ zero_extend 12) e22))))
(let ((e24 ((_ repeat 1) e23)))
(let ((e25 (ite (bvuge ((_ zero_extend 12) e3) e13) (_ bv1 1) (_ bv0 1))))
(let ((e26 ((_ zero_extend 4) e4)))
(let ((e27 (bvsle e19 e3)))
(let ((e28 (bvsle e17 e25)))
(let ((e29 (bvslt e20 ((_ zero_extend 12) e5))))
(let ((e30 (bvsge e4 e4)))
(let ((e31 (distinct e18 ((_ sign_extend 15) e7))))
(let ((e32 (bvuge e18 ((_ zero_extend 2) e26))))
(let ((e33 (bvugt e15 e24)))
(let ((e34 (bvuge e6 e4)))
(let ((e35 (bvule e13 ((_ zero_extend 12) e25))))
(let ((e36 (= ((_ zero_extend 12) e7) e12)))
(let ((e37 (= ((_ sign_extend 12) e8) e13)))
(let ((e38 (distinct e24 ((_ zero_extend 12) e17))))
(let ((e39 (bvugt e6 ((_ sign_extend 9) e7))))
(let ((e40 (bvsge v0 ((_ zero_extend 3) e20))))
(let ((e41 (bvslt ((_ sign_extend 12) e17) e20)))
(let ((e42 (bvule ((_ sign_extend 9) e22) e6)))
(let ((e43 (bvsle e3 e7)))
(let ((e44 (bvslt e12 e21)))
(let ((e45 (bvslt ((_ sign_extend 15) e17) e18)))
(let ((e46 (distinct e15 ((_ sign_extend 12) e3))))
(let ((e47 (bvult ((_ sign_extend 15) e17) v0)))
(let ((e48 (bvugt ((_ sign_extend 15) e19) v0)))
(let ((e49 (bvsge e23 e12)))
(let ((e50 (= e43 e39)))
(let ((e51 (or e27 e33)))
(let ((e52 (and e28 e37)))
(let ((e53 (= e52 e44)))
(let ((e54 (= e38 e35)))
(let ((e55 (and e51 e48)))
(let ((e56 (and e53 e36)))
(let ((e57 (ite e29 e50 e34)))
(let ((e58 (xor e45 e42)))
(let ((e59 (not e32)))
(let ((e60 (or e58 e31)))
(let ((e61 (and e46 e30)))
(let ((e62 (=> e40 e60)))
(let ((e63 (not e54)))
(let ((e64 (= e47 e55)))
(let ((e65 (=> e41 e49)))
(let ((e66 (= e62 e61)))
(let ((e67 (xor e66 e63)))
(let ((e68 (xor e67 e64)))
(let ((e69 (= e57 e65)))
(let ((e70 (and e68 e68)))
(let ((e71 (or e59 e59)))
(let ((e72 (= e69 e70)))
(let ((e73 (and e72 e56)))
(let ((e74 (and e73 e71)))
(let ((e75 (and e74 (not (= v0 (_ bv0 16))))))
(let ((e76 (and e75 (not (= v0 (bvnot (_ bv0 16)))))))
e76
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
